\begin{tabbing}
$\forall$$w$:World.
\\[0ex]FairFifo
\\[0ex]$\Rightarrow$ \=($\forall$$e$:E.\+
\\[0ex]when{-}after($e$;$\lambda$$e$.w{-}info($w$;$e$);$\lambda$$e$.w{-}pred($w$;$e$);$\lambda$$i$,$x$. s($i$;0).$x$;$\lambda$$i$.(w{-}machine($w$;$i$).2).1;$\lambda$$e$.
\\[0ex]val($e$);$\lambda$$e$.time($e$))
\\[0ex]=
\\[0ex]$<\lambda$$x$.s(loc($e$);time($e$)).$x$, $\lambda$$x$,$q$. s(loc($e$);time($e$)+1).$x$($q$ {-} 1)$>$
\\[0ex]$\in$ (:($x$:Id$\rightarrow\mathbb{Q}\rightarrow$$w$.T(loc($e$),$x$)) $\times$ ($x$:Id$\rightarrow\mathbb{Q}\rightarrow$$w$.T(loc($e$),$x$))))
\-
\end{tabbing}